H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 2.612 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule Main

((scaleFloat :: Int -> Float -> Float) :: Int -> Float -> Float)

module Main where

import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(m,_)→m

is transformed to

m0 (m,_) = m

The following Lambda expression

\(_,n)→n

is transformed to

n0 (_,n) = n

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule Main

((scaleFloat :: Int -> Float -> Float) :: Int -> Float -> Float)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Main

((scaleFloat :: Int -> Float -> Float) :: Int -> Float -> Float)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

power vx 0 = 1.0

power x vy@(y+1) = fromInt x * power x y

power x y = 1.0 / power x (`negate` y)

is transformed to

power vx xw = power4 vx xw

power x vy = power2 x vy

power x y = power0 x y

power0 x y = 1.0 / power x (`negate` y)

power1 True x vy = fromInt x * power x (vy - 1)

power1 wx wy wz = power0 wy wz

power2 x vy = power1 (vy >= 1) x vy

power2 xu xv = power0 xu xv

power3 True vx xw = 1.0

power3 xx xy xz = power2 xy xz

power4 vx xw = power3 (xw == 0) vx xw

power4 yu yv = power2 yu yv

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule Main

((scaleFloat :: Int -> Float -> Float) :: Int -> Float -> Float)

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

encodeFloat m (n + k)

where

m = m0 vu12

m0 (m,vv) = m

n = n0 vu12

n0 (vw,n) = n

vu12 = decodeFloat x

are unpacked to the following functions on top level

scaleFloatN yw = scaleFloatN0 yw (scaleFloatVu12 yw)

scaleFloatVu12 yw = decodeFloat yw

scaleFloatM0 yw (m,vv) = m

scaleFloatN0 yw (vw,n) = n

scaleFloatM yw = scaleFloatM0 yw (scaleFloatVu12 yw)

The bindings of the following Let/Where expression

fromInteger x * power 2 y

where

power vx xw = power4 vx xw

power x vy = power2 x vy

power x y = power0 x y

power0 x y = 1.0 / power x (`negate` y)

power1 True x vy = fromInt x * power x (vy - 1)

power1 wx wy wz = power0 wy wz

power2 x vy = power1 (vy >= 1) x vy

power2 xu xv = power0 xu xv

power3 True vx xw = 1.0

power3 xx xy xz = power2 xy xz

power4 vx xw = power3 (xw == 0) vx xw

power4 yu yv = power2 yu yv

are unpacked to the following functions on top level

primFloatEncodePower0 x y = 1.0 / primFloatEncodePower x (`negate` y)

primFloatEncodePower1 True x vy = fromInt x * primFloatEncodePower x (vy - 1)

primFloatEncodePower1 wx wy wz = primFloatEncodePower0 wy wz

primFloatEncodePower2 x vy = primFloatEncodePower1 (vy >= 1) x vy

primFloatEncodePower2 xu xv = primFloatEncodePower0 xu xv

primFloatEncodePower3 True vx xw = 1.0

primFloatEncodePower3 xx xy xz = primFloatEncodePower2 xy xz

primFloatEncodePower4 vx xw = primFloatEncodePower3 (xw == 0) vx xw

primFloatEncodePower4 yu yv = primFloatEncodePower2 yu yv

primFloatEncodePower vx xw = primFloatEncodePower4 vx xw

primFloatEncodePower x vy = primFloatEncodePower2 x vy

primFloatEncodePower x y = primFloatEncodePower0 x y

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

mainModule Main

((scaleFloat :: Int -> Float -> Float) :: Int -> Float -> Float)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

mainModule Main

(scaleFloat :: Int -> Float -> Float)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="scaleFloat",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="scaleFloat yx3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="scaleFloat yx3 yx4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="encodeFloat (scaleFloatM yx4) (scaleFloatN yx4 + yx3)",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="primFloatEncode (scaleFloatM yx4) (scaleFloatN yx4 + yx3)",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="fromInteger (scaleFloatM yx4) * primFloatEncodePower (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3)",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="primMulFloat (fromInteger (scaleFloatM yx4)) (primFloatEncodePower (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3))",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="primMulFloat (primIntegerToFloat (scaleFloatM yx4)) (primFloatEncodePower (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3))",fontsize=16,color="black",shape="box"];9 -> 10[label="",style="solid", color="black", weight=3];
10 -> 15[label="",style="dashed", color="red", weight=0];
10[label="primMulFloat (primIntegerToFloat (scaleFloatM0 yx4 (scaleFloatVu12 yx4))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3))",fontsize=16,color="magenta"];10 -> 16[label="",style="dashed", color="magenta", weight=3];
16[label="scaleFloatVu12 yx4",fontsize=16,color="black",shape="triangle"];16 -> 21[label="",style="solid", color="black", weight=3];
15[label="primMulFloat (primIntegerToFloat (scaleFloatM0 yx4 yx5)) (primFloatEncodePower (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3))",fontsize=16,color="burlywood",shape="triangle"];506[label="yx5/(yx50,yx51)",fontsize=10,color="white",style="solid",shape="box"];15 -> 506[label="",style="solid", color="burlywood", weight=9];
506 -> 22[label="",style="solid", color="burlywood", weight=3];
21[label="decodeFloat yx4",fontsize=16,color="black",shape="box"];21 -> 24[label="",style="solid", color="black", weight=3];
22[label="primMulFloat (primIntegerToFloat (scaleFloatM0 yx4 (yx50,yx51))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3))",fontsize=16,color="black",shape="box"];22 -> 25[label="",style="solid", color="black", weight=3];
24[label="primFloatDecode yx4",fontsize=16,color="black",shape="box"];24 -> 26[label="",style="solid", color="black", weight=3];
25[label="primMulFloat (primIntegerToFloat yx50) (primFloatEncodePower (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3))",fontsize=16,color="burlywood",shape="box"];507[label="yx50/Integer yx500",fontsize=10,color="white",style="solid",shape="box"];25 -> 507[label="",style="solid", color="burlywood", weight=9];
507 -> 27[label="",style="solid", color="burlywood", weight=3];
26[label="terminator yx4",fontsize=16,color="black",shape="box"];26 -> 28[label="",style="solid", color="black", weight=3];
27[label="primMulFloat (primIntegerToFloat (Integer yx500)) (primFloatEncodePower (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3))",fontsize=16,color="black",shape="box"];27 -> 29[label="",style="solid", color="black", weight=3];
28[label="ter1m yx4",fontsize=16,color="green",shape="box"];28 -> 30[label="",style="dashed", color="green", weight=3];
29[label="primMulFloat (primIntToFloat yx500) (primFloatEncodePower (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3))",fontsize=16,color="black",shape="box"];29 -> 31[label="",style="solid", color="black", weight=3];
30[label="yx4",fontsize=16,color="green",shape="box"];31 -> 200[label="",style="dashed", color="red", weight=0];
31[label="primMulFloat (Float yx500 (Pos (Succ Zero))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3))",fontsize=16,color="magenta"];31 -> 201[label="",style="dashed", color="magenta", weight=3];
201[label="primFloatEncodePower (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3)",fontsize=16,color="black",shape="box"];201 -> 294[label="",style="solid", color="black", weight=3];
200[label="primMulFloat (Float yx500 (Pos (Succ Zero))) yx10",fontsize=16,color="burlywood",shape="triangle"];509[label="yx10/Float yx100 yx101",fontsize=10,color="white",style="solid",shape="box"];200 -> 509[label="",style="solid", color="burlywood", weight=9];
509 -> 295[label="",style="solid", color="burlywood", weight=3];
294[label="primFloatEncodePower4 (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3)",fontsize=16,color="black",shape="box"];294 -> 296[label="",style="solid", color="black", weight=3];
295[label="primMulFloat (Float yx500 (Pos (Succ Zero))) (Float yx100 yx101)",fontsize=16,color="black",shape="box"];295 -> 297[label="",style="solid", color="black", weight=3];
296[label="primFloatEncodePower3 (scaleFloatN yx4 + yx3 == Pos Zero) (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3)",fontsize=16,color="black",shape="box"];296 -> 298[label="",style="solid", color="black", weight=3];
297[label="Float (yx500 * yx100) (Pos (Succ Zero) * yx101)",fontsize=16,color="green",shape="box"];297 -> 299[label="",style="dashed", color="green", weight=3];
297 -> 300[label="",style="dashed", color="green", weight=3];
298[label="primFloatEncodePower3 (primEqInt (scaleFloatN yx4 + yx3) (Pos Zero)) (Pos (Succ (Succ Zero))) (scaleFloatN yx4 + yx3)",fontsize=16,color="black",shape="box"];298 -> 301[label="",style="solid", color="black", weight=3];
299[label="yx500 * yx100",fontsize=16,color="black",shape="triangle"];299 -> 302[label="",style="solid", color="black", weight=3];
300 -> 299[label="",style="dashed", color="red", weight=0];
300[label="Pos (Succ Zero) * yx101",fontsize=16,color="magenta"];300 -> 303[label="",style="dashed", color="magenta", weight=3];
300 -> 304[label="",style="dashed", color="magenta", weight=3];
301[label="primFloatEncodePower3 (primEqInt (primPlusInt (scaleFloatN yx4) yx3) (Pos Zero)) (Pos (Succ (Succ Zero))) (primPlusInt (scaleFloatN yx4) yx3)",fontsize=16,color="black",shape="box"];301 -> 305[label="",style="solid", color="black", weight=3];
302[label="primMulInt yx500 yx100",fontsize=16,color="burlywood",shape="box"];511[label="yx500/Pos yx5000",fontsize=10,color="white",style="solid",shape="box"];302 -> 511[label="",style="solid", color="burlywood", weight=9];
511 -> 306[label="",style="solid", color="burlywood", weight=3];
512[label="yx500/Neg yx5000",fontsize=10,color="white",style="solid",shape="box"];302 -> 512[label="",style="solid", color="burlywood", weight=9];
512 -> 307[label="",style="solid", color="burlywood", weight=3];
303[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];304[label="yx101",fontsize=16,color="green",shape="box"];305 -> 308[label="",style="dashed", color="red", weight=0];
305[label="primFloatEncodePower3 (primEqInt (primPlusInt (scaleFloatN0 yx4 (scaleFloatVu12 yx4)) yx3) (Pos Zero)) (Pos (Succ (Succ Zero))) (primPlusInt (scaleFloatN0 yx4 (scaleFloatVu12 yx4)) yx3)",fontsize=16,color="magenta"];305 -> 309[label="",style="dashed", color="magenta", weight=3];
305 -> 310[label="",style="dashed", color="magenta", weight=3];
306[label="primMulInt (Pos yx5000) yx100",fontsize=16,color="burlywood",shape="box"];514[label="yx100/Pos yx1000",fontsize=10,color="white",style="solid",shape="box"];306 -> 514[label="",style="solid", color="burlywood", weight=9];
514 -> 311[label="",style="solid", color="burlywood", weight=3];
515[label="yx100/Neg yx1000",fontsize=10,color="white",style="solid",shape="box"];306 -> 515[label="",style="solid", color="burlywood", weight=9];
515 -> 312[label="",style="solid", color="burlywood", weight=3];
307[label="primMulInt (Neg yx5000) yx100",fontsize=16,color="burlywood",shape="box"];516[label="yx100/Pos yx1000",fontsize=10,color="white",style="solid",shape="box"];307 -> 516[label="",style="solid", color="burlywood", weight=9];
516 -> 313[label="",style="solid", color="burlywood", weight=3];
517[label="yx100/Neg yx1000",fontsize=10,color="white",style="solid",shape="box"];307 -> 517[label="",style="solid", color="burlywood", weight=9];
517 -> 314[label="",style="solid", color="burlywood", weight=3];
309 -> 16[label="",style="dashed", color="red", weight=0];
309[label="scaleFloatVu12 yx4",fontsize=16,color="magenta"];310 -> 16[label="",style="dashed", color="red", weight=0];
310[label="scaleFloatVu12 yx4",fontsize=16,color="magenta"];308[label="primFloatEncodePower3 (primEqInt (primPlusInt (scaleFloatN0 yx4 yx12) yx3) (Pos Zero)) (Pos (Succ (Succ Zero))) (primPlusInt (scaleFloatN0 yx4 yx11) yx3)",fontsize=16,color="burlywood",shape="triangle"];520[label="yx12/(yx120,yx121)",fontsize=10,color="white",style="solid",shape="box"];308 -> 520[label="",style="solid", color="burlywood", weight=9];
520 -> 315[label="",style="solid", color="burlywood", weight=3];
311[label="primMulInt (Pos yx5000) (Pos yx1000)",fontsize=16,color="black",shape="box"];311 -> 316[label="",style="solid", color="black", weight=3];
312[label="primMulInt (Pos yx5000) (Neg yx1000)",fontsize=16,color="black",shape="box"];312 -> 317[label="",style="solid", color="black", weight=3];
313[label="primMulInt (Neg yx5000) (Pos yx1000)",fontsize=16,color="black",shape="box"];313 -> 318[label="",style="solid", color="black", weight=3];
314[label="primMulInt (Neg yx5000) (Neg yx1000)",fontsize=16,color="black",shape="box"];314 -> 319[label="",style="solid", color="black", weight=3];
315[label="primFloatEncodePower3 (primEqInt (primPlusInt (scaleFloatN0 yx4 (yx120,yx121)) yx3) (Pos Zero)) (Pos (Succ (Succ Zero))) (primPlusInt (scaleFloatN0 yx4 yx11) yx3)",fontsize=16,color="black",shape="box"];315 -> 320[label="",style="solid", color="black", weight=3];
316[label="Pos (primMulNat yx5000 yx1000)",fontsize=16,color="green",shape="box"];316 -> 321[label="",style="dashed", color="green", weight=3];
317[label="Neg (primMulNat yx5000 yx1000)",fontsize=16,color="green",shape="box"];317 -> 322[label="",style="dashed", color="green", weight=3];
318[label="Neg (primMulNat yx5000 yx1000)",fontsize=16,color="green",shape="box"];318 -> 323[label="",style="dashed", color="green", weight=3];
319[label="Pos (primMulNat yx5000 yx1000)",fontsize=16,color="green",shape="box"];319 -> 324[label="",style="dashed", color="green", weight=3];
320[label="primFloatEncodePower3 (primEqInt (primPlusInt yx121 yx3) (Pos Zero)) (Pos (Succ (Succ Zero))) (primPlusInt yx121 yx3)",fontsize=16,color="burlywood",shape="box"];521[label="yx121/Pos yx1210",fontsize=10,color="white",style="solid",shape="box"];320 -> 521[label="",style="solid", color="burlywood", weight=9];
521 -> 325[label="",style="solid", color="burlywood", weight=3];
522[label="yx121/Neg yx1210",fontsize=10,color="white",style="solid",shape="box"];320 -> 522[label="",style="solid", color="burlywood", weight=9];
522 -> 326[label="",style="solid", color="burlywood", weight=3];
321[label="primMulNat yx5000 yx1000",fontsize=16,color="burlywood",shape="triangle"];523[label="yx5000/Succ yx50000",fontsize=10,color="white",style="solid",shape="box"];321 -> 523[label="",style="solid", color="burlywood", weight=9];
523 -> 327[label="",style="solid", color="burlywood", weight=3];
524[label="yx5000/Zero",fontsize=10,color="white",style="solid",shape="box"];321 -> 524[label="",style="solid", color="burlywood", weight=9];
524 -> 328[label="",style="solid", color="burlywood", weight=3];
322 -> 321[label="",style="dashed", color="red", weight=0];
322[label="primMulNat yx5000 yx1000",fontsize=16,color="magenta"];322 -> 329[label="",style="dashed", color="magenta", weight=3];
323 -> 321[label="",style="dashed", color="red", weight=0];
323[label="primMulNat yx5000 yx1000",fontsize=16,color="magenta"];323 -> 330[label="",style="dashed", color="magenta", weight=3];
324 -> 321[label="",style="dashed", color="red", weight=0];
324[label="primMulNat yx5000 yx1000",fontsize=16,color="magenta"];324 -> 331[label="",style="dashed", color="magenta", weight=3];
324 -> 332[label="",style="dashed", color="magenta", weight=3];
325[label="primFloatEncodePower3 (primEqInt (primPlusInt (Pos yx1210) yx3) (Pos Zero)) (Pos (Succ (Succ Zero))) (primPlusInt (Pos yx1210) yx3)",fontsize=16,color="burlywood",shape="box"];528[label="yx3/Pos yx30",fontsize=10,color="white",style="solid",shape="box"];325 -> 528[label="",style="solid", color="burlywood", weight=9];
528 -> 333[label="",style="solid", color="burlywood", weight=3];
529[label="yx3/Neg yx30",fontsize=10,color="white",style="solid",shape="box"];325 -> 529[label="",style="solid", color="burlywood", weight=9];
529 -> 334[label="",style="solid", color="burlywood", weight=3];
326[label="primFloatEncodePower3 (primEqInt (primPlusInt (Neg yx1210) yx3) (Pos Zero)) (Pos (Succ (Succ Zero))) (primPlusInt (Neg yx1210) yx3)",fontsize=16,color="burlywood",shape="box"];530[label="yx3/Pos yx30",fontsize=10,color="white",style="solid",shape="box"];326 -> 530[label="",style="solid", color="burlywood", weight=9];
530 -> 335[label="",style="solid", color="burlywood", weight=3];
531[label="yx3/Neg yx30",fontsize=10,color="white",style="solid",shape="box"];326 -> 531[label="",style="solid", color="burlywood", weight=9];
531 -> 336[label="",style="solid", color="burlywood", weight=3];
327[label="primMulNat (Succ yx50000) yx1000",fontsize=16,color="burlywood",shape="box"];532[label="yx1000/Succ yx10000",fontsize=10,color="white",style="solid",shape="box"];327 -> 532[label="",style="solid", color="burlywood", weight=9];
532 -> 337[label="",style="solid", color="burlywood", weight=3];
533[label="yx1000/Zero",fontsize=10,color="white",style="solid",shape="box"];327 -> 533[label="",style="solid", color="burlywood", weight=9];
533 -> 338[label="",style="solid", color="burlywood", weight=3];
328[label="primMulNat Zero yx1000",fontsize=16,color="burlywood",shape="box"];534[label="yx1000/Succ yx10000",fontsize=10,color="white",style="solid",shape="box"];328 -> 534[label="",style="solid", color="burlywood", weight=9];
534 -> 339[label="",style="solid", color="burlywood", weight=3];
535[label="yx1000/Zero",fontsize=10,color="white",style="solid",shape="box"];328 -> 535[label="",style="solid", color="burlywood", weight=9];
535 -> 340[label="",style="solid", color="burlywood", weight=3];
329[label="yx1000",fontsize=16,color="green",shape="box"];330[label="yx5000",fontsize=16,color="green",shape="box"];331[label="yx1000",fontsize=16,color="green",shape="box"];332[label="yx5000",fontsize=16,color="green",shape="box"];333[label="primFloatEncodePower3 (primEqInt (primPlusInt (Pos yx1210) (Pos yx30)) (Pos Zero)) (Pos (Succ (Succ Zero))) (primPlusInt (Pos yx1210) (Pos yx30))",fontsize=16,color="black",shape="box"];333 -> 341[label="",style="solid", color="black", weight=3];
334[label="primFloatEncodePower3 (primEqInt (primPlusInt (Pos yx1210) (Neg yx30)) (Pos Zero)) (Pos (Succ (Succ Zero))) (primPlusInt (Pos yx1210) (Neg yx30))",fontsize=16,color="black",shape="box"];334 -> 342[label="",style="solid", color="black", weight=3];
335[label="primFloatEncodePower3 (primEqInt (primPlusInt (Neg yx1210) (Pos yx30)) (Pos Zero)) (Pos (Succ (Succ Zero))) (primPlusInt (Neg yx1210) (Pos yx30))",fontsize=16,color="black",shape="box"];335 -> 343[label="",style="solid", color="black", weight=3];
336[label="primFloatEncodePower3 (primEqInt (primPlusInt (Neg yx1210) (Neg yx30)) (Pos Zero)) (Pos (Succ (Succ Zero))) (primPlusInt (Neg yx1210) (Neg yx30))",fontsize=16,color="black",shape="box"];336 -> 344[label="",style="solid", color="black", weight=3];
337[label="primMulNat (Succ yx50000) (Succ yx10000)",fontsize=16,color="black",shape="box"];337 -> 345[label="",style="solid", color="black", weight=3];
338[label="primMulNat (Succ yx50000) Zero",fontsize=16,color="black",shape="box"];338 -> 346[label="",style="solid", color="black", weight=3];
339[label="primMulNat Zero (Succ yx10000)",fontsize=16,color="black",shape="box"];339 -> 347[label="",style="solid", color="black", weight=3];
340[label="primMulNat Zero Zero",fontsize=16,color="black",shape="box"];340 -> 348[label="",style="solid", color="black", weight=3];
341[label="primFloatEncodePower3 (primEqInt (Pos (primPlusNat yx1210 yx30)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (primPlusNat yx1210 yx30))",fontsize=16,color="burlywood",shape="box"];536[label="yx1210/Succ yx12100",fontsize=10,color="white",style="solid",shape="box"];341 -> 536[label="",style="solid", color="burlywood", weight=9];
536 -> 349[label="",style="solid", color="burlywood", weight=3];
537[label="yx1210/Zero",fontsize=10,color="white",style="solid",shape="box"];341 -> 537[label="",style="solid", color="burlywood", weight=9];
537 -> 350[label="",style="solid", color="burlywood", weight=3];
342[label="primFloatEncodePower3 (primEqInt (primMinusNat yx1210 yx30) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat yx1210 yx30)",fontsize=16,color="burlywood",shape="triangle"];538[label="yx1210/Succ yx12100",fontsize=10,color="white",style="solid",shape="box"];342 -> 538[label="",style="solid", color="burlywood", weight=9];
538 -> 351[label="",style="solid", color="burlywood", weight=3];
539[label="yx1210/Zero",fontsize=10,color="white",style="solid",shape="box"];342 -> 539[label="",style="solid", color="burlywood", weight=9];
539 -> 352[label="",style="solid", color="burlywood", weight=3];
343 -> 342[label="",style="dashed", color="red", weight=0];
343[label="primFloatEncodePower3 (primEqInt (primMinusNat yx30 yx1210) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat yx30 yx1210)",fontsize=16,color="magenta"];343 -> 353[label="",style="dashed", color="magenta", weight=3];
343 -> 354[label="",style="dashed", color="magenta", weight=3];
344[label="primFloatEncodePower3 (primEqInt (Neg (primPlusNat yx1210 yx30)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (primPlusNat yx1210 yx30))",fontsize=16,color="burlywood",shape="box"];541[label="yx1210/Succ yx12100",fontsize=10,color="white",style="solid",shape="box"];344 -> 541[label="",style="solid", color="burlywood", weight=9];
541 -> 355[label="",style="solid", color="burlywood", weight=3];
542[label="yx1210/Zero",fontsize=10,color="white",style="solid",shape="box"];344 -> 542[label="",style="solid", color="burlywood", weight=9];
542 -> 356[label="",style="solid", color="burlywood", weight=3];
345 -> 357[label="",style="dashed", color="red", weight=0];
345[label="primPlusNat (primMulNat yx50000 (Succ yx10000)) (Succ yx10000)",fontsize=16,color="magenta"];345 -> 358[label="",style="dashed", color="magenta", weight=3];
346[label="Zero",fontsize=16,color="green",shape="box"];347[label="Zero",fontsize=16,color="green",shape="box"];348[label="Zero",fontsize=16,color="green",shape="box"];349[label="primFloatEncodePower3 (primEqInt (Pos (primPlusNat (Succ yx12100) yx30)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (primPlusNat (Succ yx12100) yx30))",fontsize=16,color="burlywood",shape="box"];544[label="yx30/Succ yx300",fontsize=10,color="white",style="solid",shape="box"];349 -> 544[label="",style="solid", color="burlywood", weight=9];
544 -> 359[label="",style="solid", color="burlywood", weight=3];
545[label="yx30/Zero",fontsize=10,color="white",style="solid",shape="box"];349 -> 545[label="",style="solid", color="burlywood", weight=9];
545 -> 360[label="",style="solid", color="burlywood", weight=3];
350[label="primFloatEncodePower3 (primEqInt (Pos (primPlusNat Zero yx30)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (primPlusNat Zero yx30))",fontsize=16,color="burlywood",shape="box"];546[label="yx30/Succ yx300",fontsize=10,color="white",style="solid",shape="box"];350 -> 546[label="",style="solid", color="burlywood", weight=9];
546 -> 361[label="",style="solid", color="burlywood", weight=3];
547[label="yx30/Zero",fontsize=10,color="white",style="solid",shape="box"];350 -> 547[label="",style="solid", color="burlywood", weight=9];
547 -> 362[label="",style="solid", color="burlywood", weight=3];
351[label="primFloatEncodePower3 (primEqInt (primMinusNat (Succ yx12100) yx30) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat (Succ yx12100) yx30)",fontsize=16,color="burlywood",shape="box"];548[label="yx30/Succ yx300",fontsize=10,color="white",style="solid",shape="box"];351 -> 548[label="",style="solid", color="burlywood", weight=9];
548 -> 363[label="",style="solid", color="burlywood", weight=3];
549[label="yx30/Zero",fontsize=10,color="white",style="solid",shape="box"];351 -> 549[label="",style="solid", color="burlywood", weight=9];
549 -> 364[label="",style="solid", color="burlywood", weight=3];
352[label="primFloatEncodePower3 (primEqInt (primMinusNat Zero yx30) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat Zero yx30)",fontsize=16,color="burlywood",shape="box"];550[label="yx30/Succ yx300",fontsize=10,color="white",style="solid",shape="box"];352 -> 550[label="",style="solid", color="burlywood", weight=9];
550 -> 365[label="",style="solid", color="burlywood", weight=3];
551[label="yx30/Zero",fontsize=10,color="white",style="solid",shape="box"];352 -> 551[label="",style="solid", color="burlywood", weight=9];
551 -> 366[label="",style="solid", color="burlywood", weight=3];
353[label="yx30",fontsize=16,color="green",shape="box"];354[label="yx1210",fontsize=16,color="green",shape="box"];355[label="primFloatEncodePower3 (primEqInt (Neg (primPlusNat (Succ yx12100) yx30)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (primPlusNat (Succ yx12100) yx30))",fontsize=16,color="burlywood",shape="box"];552[label="yx30/Succ yx300",fontsize=10,color="white",style="solid",shape="box"];355 -> 552[label="",style="solid", color="burlywood", weight=9];
552 -> 367[label="",style="solid", color="burlywood", weight=3];
553[label="yx30/Zero",fontsize=10,color="white",style="solid",shape="box"];355 -> 553[label="",style="solid", color="burlywood", weight=9];
553 -> 368[label="",style="solid", color="burlywood", weight=3];
356[label="primFloatEncodePower3 (primEqInt (Neg (primPlusNat Zero yx30)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (primPlusNat Zero yx30))",fontsize=16,color="burlywood",shape="box"];554[label="yx30/Succ yx300",fontsize=10,color="white",style="solid",shape="box"];356 -> 554[label="",style="solid", color="burlywood", weight=9];
554 -> 369[label="",style="solid", color="burlywood", weight=3];
555[label="yx30/Zero",fontsize=10,color="white",style="solid",shape="box"];356 -> 555[label="",style="solid", color="burlywood", weight=9];
555 -> 370[label="",style="solid", color="burlywood", weight=3];
358 -> 321[label="",style="dashed", color="red", weight=0];
358[label="primMulNat yx50000 (Succ yx10000)",fontsize=16,color="magenta"];358 -> 371[label="",style="dashed", color="magenta", weight=3];
358 -> 372[label="",style="dashed", color="magenta", weight=3];
357[label="primPlusNat yx13 (Succ yx10000)",fontsize=16,color="burlywood",shape="triangle"];557[label="yx13/Succ yx130",fontsize=10,color="white",style="solid",shape="box"];357 -> 557[label="",style="solid", color="burlywood", weight=9];
557 -> 373[label="",style="solid", color="burlywood", weight=3];
558[label="yx13/Zero",fontsize=10,color="white",style="solid",shape="box"];357 -> 558[label="",style="solid", color="burlywood", weight=9];
558 -> 374[label="",style="solid", color="burlywood", weight=3];
359[label="primFloatEncodePower3 (primEqInt (Pos (primPlusNat (Succ yx12100) (Succ yx300))) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (primPlusNat (Succ yx12100) (Succ yx300)))",fontsize=16,color="black",shape="box"];359 -> 375[label="",style="solid", color="black", weight=3];
360[label="primFloatEncodePower3 (primEqInt (Pos (primPlusNat (Succ yx12100) Zero)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (primPlusNat (Succ yx12100) Zero))",fontsize=16,color="black",shape="box"];360 -> 376[label="",style="solid", color="black", weight=3];
361[label="primFloatEncodePower3 (primEqInt (Pos (primPlusNat Zero (Succ yx300))) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (primPlusNat Zero (Succ yx300)))",fontsize=16,color="black",shape="box"];361 -> 377[label="",style="solid", color="black", weight=3];
362[label="primFloatEncodePower3 (primEqInt (Pos (primPlusNat Zero Zero)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (primPlusNat Zero Zero))",fontsize=16,color="black",shape="box"];362 -> 378[label="",style="solid", color="black", weight=3];
363[label="primFloatEncodePower3 (primEqInt (primMinusNat (Succ yx12100) (Succ yx300)) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat (Succ yx12100) (Succ yx300))",fontsize=16,color="black",shape="box"];363 -> 379[label="",style="solid", color="black", weight=3];
364[label="primFloatEncodePower3 (primEqInt (primMinusNat (Succ yx12100) Zero) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat (Succ yx12100) Zero)",fontsize=16,color="black",shape="box"];364 -> 380[label="",style="solid", color="black", weight=3];
365[label="primFloatEncodePower3 (primEqInt (primMinusNat Zero (Succ yx300)) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat Zero (Succ yx300))",fontsize=16,color="black",shape="box"];365 -> 381[label="",style="solid", color="black", weight=3];
366[label="primFloatEncodePower3 (primEqInt (primMinusNat Zero Zero) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat Zero Zero)",fontsize=16,color="black",shape="box"];366 -> 382[label="",style="solid", color="black", weight=3];
367[label="primFloatEncodePower3 (primEqInt (Neg (primPlusNat (Succ yx12100) (Succ yx300))) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (primPlusNat (Succ yx12100) (Succ yx300)))",fontsize=16,color="black",shape="box"];367 -> 383[label="",style="solid", color="black", weight=3];
368[label="primFloatEncodePower3 (primEqInt (Neg (primPlusNat (Succ yx12100) Zero)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (primPlusNat (Succ yx12100) Zero))",fontsize=16,color="black",shape="box"];368 -> 384[label="",style="solid", color="black", weight=3];
369[label="primFloatEncodePower3 (primEqInt (Neg (primPlusNat Zero (Succ yx300))) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (primPlusNat Zero (Succ yx300)))",fontsize=16,color="black",shape="box"];369 -> 385[label="",style="solid", color="black", weight=3];
370[label="primFloatEncodePower3 (primEqInt (Neg (primPlusNat Zero Zero)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (primPlusNat Zero Zero))",fontsize=16,color="black",shape="box"];370 -> 386[label="",style="solid", color="black", weight=3];
371[label="Succ yx10000",fontsize=16,color="green",shape="box"];372[label="yx50000",fontsize=16,color="green",shape="box"];373[label="primPlusNat (Succ yx130) (Succ yx10000)",fontsize=16,color="black",shape="box"];373 -> 387[label="",style="solid", color="black", weight=3];
374[label="primPlusNat Zero (Succ yx10000)",fontsize=16,color="black",shape="box"];374 -> 388[label="",style="solid", color="black", weight=3];
375[label="primFloatEncodePower3 (primEqInt (Pos (Succ (Succ (primPlusNat yx12100 yx300)))) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ (primPlusNat yx12100 yx300))))",fontsize=16,color="black",shape="box"];375 -> 389[label="",style="solid", color="black", weight=3];
376[label="primFloatEncodePower3 (primEqInt (Pos (Succ yx12100)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ yx12100))",fontsize=16,color="black",shape="triangle"];376 -> 390[label="",style="solid", color="black", weight=3];
377 -> 376[label="",style="dashed", color="red", weight=0];
377[label="primFloatEncodePower3 (primEqInt (Pos (Succ yx300)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ yx300))",fontsize=16,color="magenta"];377 -> 391[label="",style="dashed", color="magenta", weight=3];
378[label="primFloatEncodePower3 (primEqInt (Pos Zero) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos Zero)",fontsize=16,color="black",shape="triangle"];378 -> 392[label="",style="solid", color="black", weight=3];
379 -> 342[label="",style="dashed", color="red", weight=0];
379[label="primFloatEncodePower3 (primEqInt (primMinusNat yx12100 yx300) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat yx12100 yx300)",fontsize=16,color="magenta"];379 -> 393[label="",style="dashed", color="magenta", weight=3];
379 -> 394[label="",style="dashed", color="magenta", weight=3];
380 -> 376[label="",style="dashed", color="red", weight=0];
380[label="primFloatEncodePower3 (primEqInt (Pos (Succ yx12100)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ yx12100))",fontsize=16,color="magenta"];381[label="primFloatEncodePower3 (primEqInt (Neg (Succ yx300)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (Succ yx300))",fontsize=16,color="black",shape="triangle"];381 -> 395[label="",style="solid", color="black", weight=3];
382 -> 378[label="",style="dashed", color="red", weight=0];
382[label="primFloatEncodePower3 (primEqInt (Pos Zero) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos Zero)",fontsize=16,color="magenta"];383 -> 381[label="",style="dashed", color="red", weight=0];
383[label="primFloatEncodePower3 (primEqInt (Neg (Succ (Succ (primPlusNat yx12100 yx300)))) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (Succ (Succ (primPlusNat yx12100 yx300))))",fontsize=16,color="magenta"];383 -> 396[label="",style="dashed", color="magenta", weight=3];
384 -> 381[label="",style="dashed", color="red", weight=0];
384[label="primFloatEncodePower3 (primEqInt (Neg (Succ yx12100)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (Succ yx12100))",fontsize=16,color="magenta"];384 -> 397[label="",style="dashed", color="magenta", weight=3];
385 -> 381[label="",style="dashed", color="red", weight=0];
385[label="primFloatEncodePower3 (primEqInt (Neg (Succ yx300)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg (Succ yx300))",fontsize=16,color="magenta"];386[label="primFloatEncodePower3 (primEqInt (Neg Zero) (Pos Zero)) (Pos (Succ (Succ Zero))) (Neg Zero)",fontsize=16,color="black",shape="box"];386 -> 398[label="",style="solid", color="black", weight=3];
387[label="Succ (Succ (primPlusNat yx130 yx10000))",fontsize=16,color="green",shape="box"];387 -> 399[label="",style="dashed", color="green", weight=3];
388[label="Succ yx10000",fontsize=16,color="green",shape="box"];389[label="primFloatEncodePower3 False (Pos (Succ (Succ Zero))) (Pos (Succ (Succ (primPlusNat yx12100 yx300))))",fontsize=16,color="black",shape="box"];389 -> 400[label="",style="solid", color="black", weight=3];
390[label="primFloatEncodePower3 False (Pos (Succ (Succ Zero))) (Pos (Succ yx12100))",fontsize=16,color="black",shape="box"];390 -> 401[label="",style="solid", color="black", weight=3];
391[label="yx300",fontsize=16,color="green",shape="box"];392[label="primFloatEncodePower3 True (Pos (Succ (Succ Zero))) (Pos Zero)",fontsize=16,color="black",shape="box"];392 -> 402[label="",style="solid", color="black", weight=3];
393[label="yx12100",fontsize=16,color="green",shape="box"];394[label="yx300",fontsize=16,color="green",shape="box"];395[label="primFloatEncodePower3 False (Pos (Succ (Succ Zero))) (Neg (Succ yx300))",fontsize=16,color="black",shape="box"];395 -> 403[label="",style="solid", color="black", weight=3];
396[label="Succ (primPlusNat yx12100 yx300)",fontsize=16,color="green",shape="box"];396 -> 404[label="",style="dashed", color="green", weight=3];
397[label="yx12100",fontsize=16,color="green",shape="box"];398[label="primFloatEncodePower3 True (Pos (Succ (Succ Zero))) (Neg Zero)",fontsize=16,color="black",shape="box"];398 -> 405[label="",style="solid", color="black", weight=3];
399[label="primPlusNat yx130 yx10000",fontsize=16,color="burlywood",shape="triangle"];566[label="yx130/Succ yx1300",fontsize=10,color="white",style="solid",shape="box"];399 -> 566[label="",style="solid", color="burlywood", weight=9];
566 -> 406[label="",style="solid", color="burlywood", weight=3];
567[label="yx130/Zero",fontsize=10,color="white",style="solid",shape="box"];399 -> 567[label="",style="solid", color="burlywood", weight=9];
567 -> 407[label="",style="solid", color="burlywood", weight=3];
400 -> 408[label="",style="dashed", color="red", weight=0];
400[label="primFloatEncodePower2 (Pos (Succ (Succ Zero))) (Pos (Succ (Succ (primPlusNat yx12100 yx300))))",fontsize=16,color="magenta"];400 -> 409[label="",style="dashed", color="magenta", weight=3];
401[label="primFloatEncodePower2 (Pos (Succ (Succ Zero))) (Pos (Succ yx12100))",fontsize=16,color="black",shape="triangle"];401 -> 410[label="",style="solid", color="black", weight=3];
402[label="fromDouble (Double (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="triangle"];402 -> 411[label="",style="solid", color="black", weight=3];
403[label="primFloatEncodePower2 (Pos (Succ (Succ Zero))) (Neg (Succ yx300))",fontsize=16,color="black",shape="box"];403 -> 412[label="",style="solid", color="black", weight=3];
404 -> 399[label="",style="dashed", color="red", weight=0];
404[label="primPlusNat yx12100 yx300",fontsize=16,color="magenta"];404 -> 413[label="",style="dashed", color="magenta", weight=3];
404 -> 414[label="",style="dashed", color="magenta", weight=3];
405 -> 402[label="",style="dashed", color="red", weight=0];
405[label="fromDouble (Double (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="magenta"];406[label="primPlusNat (Succ yx1300) yx10000",fontsize=16,color="burlywood",shape="box"];571[label="yx10000/Succ yx100000",fontsize=10,color="white",style="solid",shape="box"];406 -> 571[label="",style="solid", color="burlywood", weight=9];
571 -> 415[label="",style="solid", color="burlywood", weight=3];
572[label="yx10000/Zero",fontsize=10,color="white",style="solid",shape="box"];406 -> 572[label="",style="solid", color="burlywood", weight=9];
572 -> 416[label="",style="solid", color="burlywood", weight=3];
407[label="primPlusNat Zero yx10000",fontsize=16,color="burlywood",shape="box"];573[label="yx10000/Succ yx100000",fontsize=10,color="white",style="solid",shape="box"];407 -> 573[label="",style="solid", color="burlywood", weight=9];
573 -> 417[label="",style="solid", color="burlywood", weight=3];
574[label="yx10000/Zero",fontsize=10,color="white",style="solid",shape="box"];407 -> 574[label="",style="solid", color="burlywood", weight=9];
574 -> 418[label="",style="solid", color="burlywood", weight=3];
409 -> 399[label="",style="dashed", color="red", weight=0];
409[label="primPlusNat yx12100 yx300",fontsize=16,color="magenta"];409 -> 419[label="",style="dashed", color="magenta", weight=3];
409 -> 420[label="",style="dashed", color="magenta", weight=3];
408 -> 401[label="",style="dashed", color="red", weight=0];
408[label="primFloatEncodePower2 (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx14)))",fontsize=16,color="magenta"];408 -> 421[label="",style="dashed", color="magenta", weight=3];
410[label="primFloatEncodePower1 (Pos (Succ yx12100) >= Pos (Succ Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ yx12100))",fontsize=16,color="black",shape="box"];410 -> 422[label="",style="solid", color="black", weight=3];
411[label="doubleToFloat (Double (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];411 -> 423[label="",style="solid", color="black", weight=3];
412[label="primFloatEncodePower1 (Neg (Succ yx300) >= Pos (Succ Zero)) (Pos (Succ (Succ Zero))) (Neg (Succ yx300))",fontsize=16,color="black",shape="box"];412 -> 424[label="",style="solid", color="black", weight=3];
413[label="yx300",fontsize=16,color="green",shape="box"];414[label="yx12100",fontsize=16,color="green",shape="box"];415[label="primPlusNat (Succ yx1300) (Succ yx100000)",fontsize=16,color="black",shape="box"];415 -> 425[label="",style="solid", color="black", weight=3];
416[label="primPlusNat (Succ yx1300) Zero",fontsize=16,color="black",shape="box"];416 -> 426[label="",style="solid", color="black", weight=3];
417[label="primPlusNat Zero (Succ yx100000)",fontsize=16,color="black",shape="box"];417 -> 427[label="",style="solid", color="black", weight=3];
418[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];418 -> 428[label="",style="solid", color="black", weight=3];
419[label="yx300",fontsize=16,color="green",shape="box"];420[label="yx12100",fontsize=16,color="green",shape="box"];421[label="Succ yx14",fontsize=16,color="green",shape="box"];422[label="primFloatEncodePower1 (compare (Pos (Succ yx12100)) (Pos (Succ Zero)) /= LT) (Pos (Succ (Succ Zero))) (Pos (Succ yx12100))",fontsize=16,color="black",shape="box"];422 -> 429[label="",style="solid", color="black", weight=3];
423[label="Float (Pos (Succ Zero)) (Pos (Succ Zero))",fontsize=16,color="green",shape="box"];424[label="primFloatEncodePower1 (compare (Neg (Succ yx300)) (Pos (Succ Zero)) /= LT) (Pos (Succ (Succ Zero))) (Neg (Succ yx300))",fontsize=16,color="black",shape="box"];424 -> 430[label="",style="solid", color="black", weight=3];
425[label="Succ (Succ (primPlusNat yx1300 yx100000))",fontsize=16,color="green",shape="box"];425 -> 431[label="",style="dashed", color="green", weight=3];
426[label="Succ yx1300",fontsize=16,color="green",shape="box"];427[label="Succ yx100000",fontsize=16,color="green",shape="box"];428[label="Zero",fontsize=16,color="green",shape="box"];429[label="primFloatEncodePower1 (not (compare (Pos (Succ yx12100)) (Pos (Succ Zero)) == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ yx12100))",fontsize=16,color="black",shape="box"];429 -> 432[label="",style="solid", color="black", weight=3];
430[label="primFloatEncodePower1 (not (compare (Neg (Succ yx300)) (Pos (Succ Zero)) == LT)) (Pos (Succ (Succ Zero))) (Neg (Succ yx300))",fontsize=16,color="black",shape="box"];430 -> 433[label="",style="solid", color="black", weight=3];
431 -> 399[label="",style="dashed", color="red", weight=0];
431[label="primPlusNat yx1300 yx100000",fontsize=16,color="magenta"];431 -> 434[label="",style="dashed", color="magenta", weight=3];
431 -> 435[label="",style="dashed", color="magenta", weight=3];
432[label="primFloatEncodePower1 (not (primCmpInt (Pos (Succ yx12100)) (Pos (Succ Zero)) == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ yx12100))",fontsize=16,color="black",shape="box"];432 -> 436[label="",style="solid", color="black", weight=3];
433[label="primFloatEncodePower1 (not (primCmpInt (Neg (Succ yx300)) (Pos (Succ Zero)) == LT)) (Pos (Succ (Succ Zero))) (Neg (Succ yx300))",fontsize=16,color="black",shape="box"];433 -> 437[label="",style="solid", color="black", weight=3];
434[label="yx100000",fontsize=16,color="green",shape="box"];435[label="yx1300",fontsize=16,color="green",shape="box"];436[label="primFloatEncodePower1 (not (primCmpNat (Succ yx12100) (Succ Zero) == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ yx12100))",fontsize=16,color="black",shape="box"];436 -> 438[label="",style="solid", color="black", weight=3];
437[label="primFloatEncodePower1 (not (LT == LT)) (Pos (Succ (Succ Zero))) (Neg (Succ yx300))",fontsize=16,color="black",shape="box"];437 -> 439[label="",style="solid", color="black", weight=3];
438[label="primFloatEncodePower1 (not (primCmpNat yx12100 Zero == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ yx12100))",fontsize=16,color="burlywood",shape="box"];578[label="yx12100/Succ yx121000",fontsize=10,color="white",style="solid",shape="box"];438 -> 578[label="",style="solid", color="burlywood", weight=9];
578 -> 440[label="",style="solid", color="burlywood", weight=3];
579[label="yx12100/Zero",fontsize=10,color="white",style="solid",shape="box"];438 -> 579[label="",style="solid", color="burlywood", weight=9];
579 -> 441[label="",style="solid", color="burlywood", weight=3];
439[label="primFloatEncodePower1 (not True) (Pos (Succ (Succ Zero))) (Neg (Succ yx300))",fontsize=16,color="black",shape="box"];439 -> 442[label="",style="solid", color="black", weight=3];
440[label="primFloatEncodePower1 (not (primCmpNat (Succ yx121000) Zero == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx121000)))",fontsize=16,color="black",shape="box"];440 -> 443[label="",style="solid", color="black", weight=3];
441[label="primFloatEncodePower1 (not (primCmpNat Zero Zero == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];441 -> 444[label="",style="solid", color="black", weight=3];
442[label="primFloatEncodePower1 False (Pos (Succ (Succ Zero))) (Neg (Succ yx300))",fontsize=16,color="black",shape="box"];442 -> 445[label="",style="solid", color="black", weight=3];
443[label="primFloatEncodePower1 (not (GT == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx121000)))",fontsize=16,color="black",shape="box"];443 -> 446[label="",style="solid", color="black", weight=3];
444[label="primFloatEncodePower1 (not (EQ == LT)) (Pos (Succ (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];444 -> 447[label="",style="solid", color="black", weight=3];
445[label="primFloatEncodePower0 (Pos (Succ (Succ Zero))) (Neg (Succ yx300))",fontsize=16,color="black",shape="box"];445 -> 448[label="",style="solid", color="black", weight=3];
446[label="primFloatEncodePower1 (not False) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx121000)))",fontsize=16,color="black",shape="box"];446 -> 449[label="",style="solid", color="black", weight=3];
447[label="primFloatEncodePower1 (not False) (Pos (Succ (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];447 -> 450[label="",style="solid", color="black", weight=3];
448 -> 451[label="",style="dashed", color="red", weight=0];
448[label="fromDouble (Double (Pos (Succ Zero)) (Pos (Succ Zero))) / primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx300))",fontsize=16,color="magenta"];448 -> 452[label="",style="dashed", color="magenta", weight=3];
449[label="primFloatEncodePower1 True (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx121000)))",fontsize=16,color="black",shape="box"];449 -> 453[label="",style="solid", color="black", weight=3];
450[label="primFloatEncodePower1 True (Pos (Succ (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];450 -> 454[label="",style="solid", color="black", weight=3];
452 -> 402[label="",style="dashed", color="red", weight=0];
452[label="fromDouble (Double (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="magenta"];451[label="yx15 / primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx300))",fontsize=16,color="black",shape="triangle"];451 -> 455[label="",style="solid", color="black", weight=3];
453[label="fromInt (Pos (Succ (Succ Zero))) * primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx121000)) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];453 -> 456[label="",style="solid", color="black", weight=3];
454[label="fromInt (Pos (Succ (Succ Zero))) * primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];454 -> 457[label="",style="solid", color="black", weight=3];
455[label="primDivFloat yx15 (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx300)))",fontsize=16,color="burlywood",shape="box"];582[label="yx15/Float yx150 yx151",fontsize=10,color="white",style="solid",shape="box"];455 -> 582[label="",style="solid", color="burlywood", weight=9];
582 -> 458[label="",style="solid", color="burlywood", weight=3];
456[label="primMulFloat (fromInt (Pos (Succ (Succ Zero)))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx121000)) - Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];456 -> 459[label="",style="solid", color="black", weight=3];
457[label="primMulFloat (fromInt (Pos (Succ (Succ Zero)))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];457 -> 460[label="",style="solid", color="black", weight=3];
458[label="primDivFloat (Float yx150 yx151) (primFloatEncodePower (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx300)))",fontsize=16,color="black",shape="box"];458 -> 461[label="",style="solid", color="black", weight=3];
459[label="primMulFloat (primIntToFloat (Pos (Succ (Succ Zero)))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx121000)) - Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];459 -> 462[label="",style="solid", color="black", weight=3];
460[label="primMulFloat (primIntToFloat (Pos (Succ (Succ Zero)))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];460 -> 463[label="",style="solid", color="black", weight=3];
461 -> 478[label="",style="dashed", color="red", weight=0];
461[label="primDivFloat (Float yx150 yx151) (primFloatEncodePower4 (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx300)))",fontsize=16,color="magenta"];461 -> 479[label="",style="dashed", color="magenta", weight=3];
462 -> 200[label="",style="dashed", color="red", weight=0];
462[label="primMulFloat (Float (Pos (Succ (Succ Zero))) (Pos (Succ Zero))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx121000)) - Pos (Succ Zero)))",fontsize=16,color="magenta"];462 -> 465[label="",style="dashed", color="magenta", weight=3];
462 -> 466[label="",style="dashed", color="magenta", weight=3];
463 -> 200[label="",style="dashed", color="red", weight=0];
463[label="primMulFloat (Float (Pos (Succ (Succ Zero))) (Pos (Succ Zero))) (primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero)))",fontsize=16,color="magenta"];463 -> 467[label="",style="dashed", color="magenta", weight=3];
463 -> 468[label="",style="dashed", color="magenta", weight=3];
479[label="primFloatEncodePower4 (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx300))",fontsize=16,color="black",shape="box"];479 -> 484[label="",style="solid", color="black", weight=3];
478[label="primDivFloat (Float yx150 yx151) yx16",fontsize=16,color="burlywood",shape="triangle"];586[label="yx16/Float yx160 yx161",fontsize=10,color="white",style="solid",shape="box"];478 -> 586[label="",style="solid", color="burlywood", weight=9];
586 -> 485[label="",style="solid", color="burlywood", weight=3];
465[label="Pos (Succ (Succ Zero))",fontsize=16,color="green",shape="box"];466[label="primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx121000)) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];466 -> 470[label="",style="solid", color="black", weight=3];
467[label="Pos (Succ (Succ Zero))",fontsize=16,color="green",shape="box"];468[label="primFloatEncodePower (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];468 -> 471[label="",style="solid", color="black", weight=3];
484[label="primFloatEncodePower3 (`negate` Neg (Succ yx300) == Pos Zero) (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx300))",fontsize=16,color="black",shape="box"];484 -> 488[label="",style="solid", color="black", weight=3];
485[label="primDivFloat (Float yx150 yx151) (Float yx160 yx161)",fontsize=16,color="black",shape="box"];485 -> 489[label="",style="solid", color="black", weight=3];
470[label="primFloatEncodePower4 (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx121000)) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];470 -> 473[label="",style="solid", color="black", weight=3];
471[label="primFloatEncodePower4 (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];471 -> 474[label="",style="solid", color="black", weight=3];
488[label="primFloatEncodePower3 (primEqInt (`negate` Neg (Succ yx300)) (Pos Zero)) (Pos (Succ (Succ Zero))) (`negate` Neg (Succ yx300))",fontsize=16,color="black",shape="box"];488 -> 492[label="",style="solid", color="black", weight=3];
489[label="Float (yx150 * yx161) (yx151 * yx160)",fontsize=16,color="green",shape="box"];489 -> 493[label="",style="dashed", color="green", weight=3];
489 -> 494[label="",style="dashed", color="green", weight=3];
473[label="primFloatEncodePower3 (Pos (Succ (Succ yx121000)) - Pos (Succ Zero) == Pos Zero) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx121000)) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];473 -> 476[label="",style="solid", color="black", weight=3];
474[label="primFloatEncodePower3 (Pos (Succ Zero) - Pos (Succ Zero) == Pos Zero) (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];474 -> 477[label="",style="solid", color="black", weight=3];
492[label="primFloatEncodePower3 (primEqInt (primNegInt (Neg (Succ yx300))) (Pos Zero)) (Pos (Succ (Succ Zero))) (primNegInt (Neg (Succ yx300)))",fontsize=16,color="black",shape="box"];492 -> 499[label="",style="solid", color="black", weight=3];
493 -> 299[label="",style="dashed", color="red", weight=0];
493[label="yx150 * yx161",fontsize=16,color="magenta"];493 -> 500[label="",style="dashed", color="magenta", weight=3];
493 -> 501[label="",style="dashed", color="magenta", weight=3];
494 -> 299[label="",style="dashed", color="red", weight=0];
494[label="yx151 * yx160",fontsize=16,color="magenta"];494 -> 502[label="",style="dashed", color="magenta", weight=3];
494 -> 503[label="",style="dashed", color="magenta", weight=3];
476[label="primFloatEncodePower3 (primEqInt (Pos (Succ (Succ yx121000)) - Pos (Succ Zero)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ (Succ yx121000)) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];476 -> 486[label="",style="solid", color="black", weight=3];
477[label="primFloatEncodePower3 (primEqInt (Pos (Succ Zero) - Pos (Succ Zero)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ Zero) - Pos (Succ Zero))",fontsize=16,color="black",shape="box"];477 -> 487[label="",style="solid", color="black", weight=3];
499 -> 376[label="",style="dashed", color="red", weight=0];
499[label="primFloatEncodePower3 (primEqInt (Pos (Succ yx300)) (Pos Zero)) (Pos (Succ (Succ Zero))) (Pos (Succ yx300))",fontsize=16,color="magenta"];499 -> 504[label="",style="dashed", color="magenta", weight=3];
500[label="yx150",fontsize=16,color="green",shape="box"];501[label="yx161",fontsize=16,color="green",shape="box"];502[label="yx151",fontsize=16,color="green",shape="box"];503[label="yx160",fontsize=16,color="green",shape="box"];486[label="primFloatEncodePower3 (primEqInt (primMinusInt (Pos (Succ (Succ yx121000))) (Pos (Succ Zero))) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusInt (Pos (Succ (Succ yx121000))) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];486 -> 490[label="",style="solid", color="black", weight=3];
487[label="primFloatEncodePower3 (primEqInt (primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusInt (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];487 -> 491[label="",style="solid", color="black", weight=3];
504[label="yx300",fontsize=16,color="green",shape="box"];490 -> 342[label="",style="dashed", color="red", weight=0];
490[label="primFloatEncodePower3 (primEqInt (primMinusNat (Succ (Succ yx121000)) (Succ Zero)) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat (Succ (Succ yx121000)) (Succ Zero))",fontsize=16,color="magenta"];490 -> 495[label="",style="dashed", color="magenta", weight=3];
490 -> 496[label="",style="dashed", color="magenta", weight=3];
491 -> 342[label="",style="dashed", color="red", weight=0];
491[label="primFloatEncodePower3 (primEqInt (primMinusNat (Succ Zero) (Succ Zero)) (Pos Zero)) (Pos (Succ (Succ Zero))) (primMinusNat (Succ Zero) (Succ Zero))",fontsize=16,color="magenta"];491 -> 497[label="",style="dashed", color="magenta", weight=3];
491 -> 498[label="",style="dashed", color="magenta", weight=3];
495[label="Succ (Succ yx121000)",fontsize=16,color="green",shape="box"];496[label="Succ Zero",fontsize=16,color="green",shape="box"];497[label="Succ Zero",fontsize=16,color="green",shape="box"];498[label="Succ Zero",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                          ↳ QDP

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yx1300), Succ(yx100000)) → new_primPlusNat(yx1300, yx100000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(yx1300), Succ(yx100000)) → new_primPlusNat(yx1300, yx100000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yx50000), Succ(yx10000)) → new_primMulNat(yx50000, Succ(yx10000))

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(yx50000), Succ(yx10000)) → new_primMulNat(yx50000, Succ(yx10000))
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_fs(Float(yx150, yx151), yx300) → new_primFloatEncodePower30(yx300)
new_primFloatEncodePower3(Succ(yx12100), Succ(yx300)) → new_primFloatEncodePower3(yx12100, yx300)
new_primFloatEncodePower2(Succ(yx121000)) → new_primFloatEncodePower3(Succ(Succ(yx121000)), Succ(Zero))
new_primFloatEncodePower3(Zero, Succ(yx300)) → new_fs(new_fromDouble, yx300)
new_primFloatEncodePower30(Zero) → new_primFloatEncodePower3(Succ(Zero), Succ(Zero))
new_primFloatEncodePower30(Succ(yx121000)) → new_primFloatEncodePower3(Succ(Succ(yx121000)), Succ(Zero))
new_primFloatEncodePower2(Zero) → new_primFloatEncodePower3(Succ(Zero), Succ(Zero))
new_primFloatEncodePower31(yx300) → new_fs(new_fromDouble, yx300)
new_primFloatEncodePower3(Succ(yx12100), Zero) → new_primFloatEncodePower30(yx12100)

The TRS R consists of the following rules:

new_fromDouble → Float(Pos(Succ(Zero)), Pos(Succ(Zero)))

The set Q consists of the following terms:

new_fromDouble

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

new_fs(Float(yx150, yx151), yx300) → new_primFloatEncodePower30(yx300)
new_primFloatEncodePower3(Succ(yx12100), Succ(yx300)) → new_primFloatEncodePower3(yx12100, yx300)
new_primFloatEncodePower3(Zero, Succ(yx300)) → new_fs(new_fromDouble, yx300)
new_primFloatEncodePower30(Zero) → new_primFloatEncodePower3(Succ(Zero), Succ(Zero))
new_primFloatEncodePower30(Succ(yx121000)) → new_primFloatEncodePower3(Succ(Succ(yx121000)), Succ(Zero))
new_primFloatEncodePower3(Succ(yx12100), Zero) → new_primFloatEncodePower30(yx12100)

The TRS R consists of the following rules:

new_fromDouble → Float(Pos(Succ(Zero)), Pos(Succ(Zero)))

The set Q consists of the following terms:

new_fromDouble

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primFloatEncodePower3(Zero, Succ(yx300)) → new_fs(new_fromDouble, yx300) at position [0] we obtained the following new rules:

new_primFloatEncodePower3(Zero, Succ(yx300)) → new_fs(Float(Pos(Succ(Zero)), Pos(Succ(Zero))), yx300)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_fs(Float(yx150, yx151), yx300) → new_primFloatEncodePower30(yx300)
new_primFloatEncodePower3(Succ(yx12100), Succ(yx300)) → new_primFloatEncodePower3(yx12100, yx300)
new_primFloatEncodePower30(Zero) → new_primFloatEncodePower3(Succ(Zero), Succ(Zero))
new_primFloatEncodePower30(Succ(yx121000)) → new_primFloatEncodePower3(Succ(Succ(yx121000)), Succ(Zero))
new_primFloatEncodePower3(Zero, Succ(yx300)) → new_fs(Float(Pos(Succ(Zero)), Pos(Succ(Zero))), yx300)
new_primFloatEncodePower3(Succ(yx12100), Zero) → new_primFloatEncodePower30(yx12100)

The TRS R consists of the following rules:

new_fromDouble → Float(Pos(Succ(Zero)), Pos(Succ(Zero)))

The set Q consists of the following terms:

new_fromDouble

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_fs(Float(yx150, yx151), yx300) → new_primFloatEncodePower30(yx300)
new_primFloatEncodePower3(Succ(yx12100), Succ(yx300)) → new_primFloatEncodePower3(yx12100, yx300)
new_primFloatEncodePower30(Zero) → new_primFloatEncodePower3(Succ(Zero), Succ(Zero))
new_primFloatEncodePower30(Succ(yx121000)) → new_primFloatEncodePower3(Succ(Succ(yx121000)), Succ(Zero))
new_primFloatEncodePower3(Zero, Succ(yx300)) → new_fs(Float(Pos(Succ(Zero)), Pos(Succ(Zero))), yx300)
new_primFloatEncodePower3(Succ(yx12100), Zero) → new_primFloatEncodePower30(yx12100)

R is empty.
The set Q consists of the following terms:

new_fromDouble

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_fromDouble

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ QReductionProof

                                          ↳ QDP

                                            ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

new_fs(Float(yx150, yx151), yx300) → new_primFloatEncodePower30(yx300)
new_primFloatEncodePower3(Succ(yx12100), Succ(yx300)) → new_primFloatEncodePower3(yx12100, yx300)
new_primFloatEncodePower30(Zero) → new_primFloatEncodePower3(Succ(Zero), Succ(Zero))
new_primFloatEncodePower30(Succ(yx121000)) → new_primFloatEncodePower3(Succ(Succ(yx121000)), Succ(Zero))
new_primFloatEncodePower3(Zero, Succ(yx300)) → new_fs(Float(Pos(Succ(Zero)), Pos(Succ(Zero))), yx300)
new_primFloatEncodePower3(Succ(yx12100), Zero) → new_primFloatEncodePower30(yx12100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule new_fs(Float(yx150, yx151), yx300) → new_primFloatEncodePower30(yx300) we obtained the following new rules:

new_fs(Float(Pos(Succ(Zero)), Pos(Succ(Zero))), z0) → new_primFloatEncodePower30(z0)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ QReductionProof

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

new_fs(Float(Pos(Succ(Zero)), Pos(Succ(Zero))), z0) → new_primFloatEncodePower30(z0)
new_primFloatEncodePower3(Succ(yx12100), Succ(yx300)) → new_primFloatEncodePower3(yx12100, yx300)
new_primFloatEncodePower30(Zero) → new_primFloatEncodePower3(Succ(Zero), Succ(Zero))
new_primFloatEncodePower30(Succ(yx121000)) → new_primFloatEncodePower3(Succ(Succ(yx121000)), Succ(Zero))
new_primFloatEncodePower3(Zero, Succ(yx300)) → new_fs(Float(Pos(Succ(Zero)), Pos(Succ(Zero))), yx300)
new_primFloatEncodePower3(Succ(yx12100), Zero) → new_primFloatEncodePower30(yx12100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule new_primFloatEncodePower3(Succ(yx12100), Succ(yx300)) → new_primFloatEncodePower3(yx12100, yx300) we obtained the following new rules:

new_primFloatEncodePower3(Succ(Succ(y_0)), Succ(Succ(y_1))) → new_primFloatEncodePower3(Succ(y_0), Succ(y_1))
new_primFloatEncodePower3(Succ(Zero), Succ(Succ(y_0))) → new_primFloatEncodePower3(Zero, Succ(y_0))
new_primFloatEncodePower3(Succ(Succ(y_0)), Succ(Zero)) → new_primFloatEncodePower3(Succ(y_0), Zero)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ QReductionProof

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ ForwardInstantiation

                                                  ↳ QDP

                                                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_fs(Float(Pos(Succ(Zero)), Pos(Succ(Zero))), z0) → new_primFloatEncodePower30(z0)
new_primFloatEncodePower3(Succ(Succ(y_0)), Succ(Succ(y_1))) → new_primFloatEncodePower3(Succ(y_0), Succ(y_1))
new_primFloatEncodePower30(Zero) → new_primFloatEncodePower3(Succ(Zero), Succ(Zero))
new_primFloatEncodePower30(Succ(yx121000)) → new_primFloatEncodePower3(Succ(Succ(yx121000)), Succ(Zero))
new_primFloatEncodePower3(Succ(Succ(y_0)), Succ(Zero)) → new_primFloatEncodePower3(Succ(y_0), Zero)
new_primFloatEncodePower3(Succ(Zero), Succ(Succ(y_0))) → new_primFloatEncodePower3(Zero, Succ(y_0))
new_primFloatEncodePower3(Zero, Succ(yx300)) → new_fs(Float(Pos(Succ(Zero)), Pos(Succ(Zero))), yx300)
new_primFloatEncodePower3(Succ(yx12100), Zero) → new_primFloatEncodePower30(yx12100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 4 less nodes.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ QReductionProof

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ ForwardInstantiation

                                                  ↳ QDP

                                                    ↳ DependencyGraphProof

                                                      ↳ AND

                                                        ↳ QDP

                                                          ↳ ForwardInstantiation

                                                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primFloatEncodePower30(Succ(yx121000)) → new_primFloatEncodePower3(Succ(Succ(yx121000)), Succ(Zero))
new_primFloatEncodePower3(Succ(Succ(y_0)), Succ(Zero)) → new_primFloatEncodePower3(Succ(y_0), Zero)
new_primFloatEncodePower3(Succ(yx12100), Zero) → new_primFloatEncodePower30(yx12100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule new_primFloatEncodePower3(Succ(yx12100), Zero) → new_primFloatEncodePower30(yx12100) we obtained the following new rules:

new_primFloatEncodePower3(Succ(Succ(y_0)), Zero) → new_primFloatEncodePower30(Succ(y_0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ QReductionProof

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ ForwardInstantiation

                                                  ↳ QDP

                                                    ↳ DependencyGraphProof

                                                      ↳ AND

                                                        ↳ QDP

                                                          ↳ ForwardInstantiation

                                                            ↳ QDP

                                                              ↳ QDPOrderProof

                                                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primFloatEncodePower3(Succ(Succ(y_0)), Zero) → new_primFloatEncodePower30(Succ(y_0))
new_primFloatEncodePower30(Succ(yx121000)) → new_primFloatEncodePower3(Succ(Succ(yx121000)), Succ(Zero))
new_primFloatEncodePower3(Succ(Succ(y_0)), Succ(Zero)) → new_primFloatEncodePower3(Succ(y_0), Zero)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_primFloatEncodePower30(Succ(yx121000)) → new_primFloatEncodePower3(Succ(Succ(yx121000)), Succ(Zero))

The remaining pairs can at least be oriented weakly.

new_primFloatEncodePower3(Succ(Succ(y_0)), Zero) → new_primFloatEncodePower30(Succ(y_0))
new_primFloatEncodePower3(Succ(Succ(y_0)), Succ(Zero)) → new_primFloatEncodePower3(Succ(y_0), Zero)

Used ordering: Matrix interpretation [3]:
Non-tuple symbols:

M( Succ(x₁) ) =

/	1	\
\	0	/

/	1	0	\
\	1	0	/

x₁

M( Zero ) =

/	0	\
\	1	/

Tuple symbols:

M( new_primFloatEncodePower3(x₁, x₂) ) =

[

]

x₁

[

]

x₂

M( new_primFloatEncodePower30(x₁) ) =

[

]

x₁

Matrix type:
We used a basic matrix type which is not further parametrizeable.

As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented: none

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ QReductionProof

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ ForwardInstantiation

                                                  ↳ QDP

                                                    ↳ DependencyGraphProof

                                                      ↳ AND

                                                        ↳ QDP

                                                          ↳ ForwardInstantiation

                                                            ↳ QDP

                                                              ↳ QDPOrderProof

                                                                ↳ QDP

                                                                  ↳ DependencyGraphProof

                                                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primFloatEncodePower3(Succ(Succ(y_0)), Zero) → new_primFloatEncodePower30(Succ(y_0))
new_primFloatEncodePower3(Succ(Succ(y_0)), Succ(Zero)) → new_primFloatEncodePower3(Succ(y_0), Zero)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ QReductionProof

                                          ↳ QDP

                                            ↳ Instantiation

                                              ↳ QDP

                                                ↳ ForwardInstantiation

                                                  ↳ QDP

                                                    ↳ DependencyGraphProof

                                                      ↳ AND

                                                        ↳ QDP

                                                        ↳ QDP

                                                          ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primFloatEncodePower3(Succ(Succ(y_0)), Succ(Succ(y_1))) → new_primFloatEncodePower3(Succ(y_0), Succ(y_1))

From the DPs we obtained the following set of size-change graphs:

new_primFloatEncodePower3(Succ(Succ(y_0)), Succ(Succ(y_1))) → new_primFloatEncodePower3(Succ(y_0), Succ(y_1))
The graph contains the following edges 1 > 1, 2 > 2

power	vx 0	= 1.0
power	x vy@(y+1)	= fromInt x * power x y
power	x y	= 1.0 / power x (`negate` y)

power	vx xw	= power4 vx xw
power	x vy	= power2 x vy
power	x y	= power0 x y

power1	True x vy	= fromInt x * power x (vy - 1)
power1	wx wy wz	= power0 wy wz

power4	vx xw	= power3 (xw == 0) vx xw
power4	yu yv	= power2 yu yv

primFloatEncodePower1	True x vy	= fromInt x * primFloatEncodePower x (vy - 1)
primFloatEncodePower1	wx wy wz	= primFloatEncodePower0 wy wz

primFloatEncodePower2	x vy	= primFloatEncodePower1 (vy >= 1) x vy
primFloatEncodePower2	xu xv	= primFloatEncodePower0 xu xv

primFloatEncodePower3	True vx xw	= 1.0
primFloatEncodePower3	xx xy xz	= primFloatEncodePower2 xy xz

primFloatEncodePower4	vx xw	= primFloatEncodePower3 (xw == 0) vx xw
primFloatEncodePower4	yu yv	= primFloatEncodePower2 yu yv

primFloatEncodePower	vx xw	= primFloatEncodePower4 vx xw
primFloatEncodePower	x vy	= primFloatEncodePower2 x vy
primFloatEncodePower	x y	= primFloatEncodePower0 x y